Termination w.r.t. Q of the following Term Rewriting System could not be shown:
Q restricted rewrite system:
The TRS R consists of the following rules:
fstsplit2(0, x) -> nil
fstsplit2(s1(n), nil) -> nil
fstsplit2(s1(n), cons2(h, t)) -> cons2(h, fstsplit2(n, t))
sndsplit2(0, x) -> x
sndsplit2(s1(n), nil) -> nil
sndsplit2(s1(n), cons2(h, t)) -> sndsplit2(n, t)
empty1(nil) -> true
empty1(cons2(h, t)) -> false
leq2(0, m) -> true
leq2(s1(n), 0) -> false
leq2(s1(n), s1(m)) -> leq2(n, m)
length1(nil) -> 0
length1(cons2(h, t)) -> s1(length1(t))
app2(nil, x) -> x
app2(cons2(h, t), x) -> cons2(h, app2(t, x))
map_f2(pid, nil) -> nil
map_f2(pid, cons2(h, t)) -> app2(f2(pid, h), map_f2(pid, t))
process2(store, m) -> if13(store, m, leq2(m, length1(store)))
if13(store, m, true) -> if23(store, m, empty1(fstsplit2(m, store)))
if13(store, m, false) -> if33(store, m, empty1(fstsplit2(m, app2(map_f2(self, nil), store))))
if23(store, m, false) -> process2(app2(map_f2(self, nil), sndsplit2(m, store)), m)
if33(store, m, false) -> process2(sndsplit2(m, app2(map_f2(self, nil), store)), m)
Q is empty.
↳ QTRS
↳ Non-Overlap Check
Q restricted rewrite system:
The TRS R consists of the following rules:
fstsplit2(0, x) -> nil
fstsplit2(s1(n), nil) -> nil
fstsplit2(s1(n), cons2(h, t)) -> cons2(h, fstsplit2(n, t))
sndsplit2(0, x) -> x
sndsplit2(s1(n), nil) -> nil
sndsplit2(s1(n), cons2(h, t)) -> sndsplit2(n, t)
empty1(nil) -> true
empty1(cons2(h, t)) -> false
leq2(0, m) -> true
leq2(s1(n), 0) -> false
leq2(s1(n), s1(m)) -> leq2(n, m)
length1(nil) -> 0
length1(cons2(h, t)) -> s1(length1(t))
app2(nil, x) -> x
app2(cons2(h, t), x) -> cons2(h, app2(t, x))
map_f2(pid, nil) -> nil
map_f2(pid, cons2(h, t)) -> app2(f2(pid, h), map_f2(pid, t))
process2(store, m) -> if13(store, m, leq2(m, length1(store)))
if13(store, m, true) -> if23(store, m, empty1(fstsplit2(m, store)))
if13(store, m, false) -> if33(store, m, empty1(fstsplit2(m, app2(map_f2(self, nil), store))))
if23(store, m, false) -> process2(app2(map_f2(self, nil), sndsplit2(m, store)), m)
if33(store, m, false) -> process2(sndsplit2(m, app2(map_f2(self, nil), store)), m)
Q is empty.
The TRS is non-overlapping. Hence, we can switch to innermost.
↳ QTRS
↳ Non-Overlap Check
↳ QTRS
↳ DependencyPairsProof
Q restricted rewrite system:
The TRS R consists of the following rules:
fstsplit2(0, x) -> nil
fstsplit2(s1(n), nil) -> nil
fstsplit2(s1(n), cons2(h, t)) -> cons2(h, fstsplit2(n, t))
sndsplit2(0, x) -> x
sndsplit2(s1(n), nil) -> nil
sndsplit2(s1(n), cons2(h, t)) -> sndsplit2(n, t)
empty1(nil) -> true
empty1(cons2(h, t)) -> false
leq2(0, m) -> true
leq2(s1(n), 0) -> false
leq2(s1(n), s1(m)) -> leq2(n, m)
length1(nil) -> 0
length1(cons2(h, t)) -> s1(length1(t))
app2(nil, x) -> x
app2(cons2(h, t), x) -> cons2(h, app2(t, x))
map_f2(pid, nil) -> nil
map_f2(pid, cons2(h, t)) -> app2(f2(pid, h), map_f2(pid, t))
process2(store, m) -> if13(store, m, leq2(m, length1(store)))
if13(store, m, true) -> if23(store, m, empty1(fstsplit2(m, store)))
if13(store, m, false) -> if33(store, m, empty1(fstsplit2(m, app2(map_f2(self, nil), store))))
if23(store, m, false) -> process2(app2(map_f2(self, nil), sndsplit2(m, store)), m)
if33(store, m, false) -> process2(sndsplit2(m, app2(map_f2(self, nil), store)), m)
The set Q consists of the following terms:
fstsplit2(0, x0)
fstsplit2(s1(x0), nil)
fstsplit2(s1(x0), cons2(x1, x2))
sndsplit2(0, x0)
sndsplit2(s1(x0), nil)
sndsplit2(s1(x0), cons2(x1, x2))
empty1(nil)
empty1(cons2(x0, x1))
leq2(0, x0)
leq2(s1(x0), 0)
leq2(s1(x0), s1(x1))
length1(nil)
length1(cons2(x0, x1))
app2(nil, x0)
app2(cons2(x0, x1), x2)
map_f2(x0, nil)
map_f2(x0, cons2(x1, x2))
process2(x0, x1)
if13(x0, x1, true)
if13(x0, x1, false)
if23(x0, x1, false)
if33(x0, x1, false)
Q DP problem:
The TRS P consists of the following rules:
IF33(store, m, false) -> SNDSPLIT2(m, app2(map_f2(self, nil), store))
PROCESS2(store, m) -> LENGTH1(store)
SNDSPLIT2(s1(n), cons2(h, t)) -> SNDSPLIT2(n, t)
IF23(store, m, false) -> PROCESS2(app2(map_f2(self, nil), sndsplit2(m, store)), m)
IF33(store, m, false) -> PROCESS2(sndsplit2(m, app2(map_f2(self, nil), store)), m)
IF23(store, m, false) -> APP2(map_f2(self, nil), sndsplit2(m, store))
IF13(store, m, true) -> FSTSPLIT2(m, store)
IF23(store, m, false) -> MAP_F2(self, nil)
MAP_F2(pid, cons2(h, t)) -> APP2(f2(pid, h), map_f2(pid, t))
IF13(store, m, true) -> EMPTY1(fstsplit2(m, store))
PROCESS2(store, m) -> IF13(store, m, leq2(m, length1(store)))
IF33(store, m, false) -> APP2(map_f2(self, nil), store)
FSTSPLIT2(s1(n), cons2(h, t)) -> FSTSPLIT2(n, t)
IF13(store, m, true) -> IF23(store, m, empty1(fstsplit2(m, store)))
IF13(store, m, false) -> MAP_F2(self, nil)
IF13(store, m, false) -> FSTSPLIT2(m, app2(map_f2(self, nil), store))
IF13(store, m, false) -> EMPTY1(fstsplit2(m, app2(map_f2(self, nil), store)))
APP2(cons2(h, t), x) -> APP2(t, x)
IF33(store, m, false) -> MAP_F2(self, nil)
LENGTH1(cons2(h, t)) -> LENGTH1(t)
IF23(store, m, false) -> SNDSPLIT2(m, store)
PROCESS2(store, m) -> LEQ2(m, length1(store))
IF13(store, m, false) -> IF33(store, m, empty1(fstsplit2(m, app2(map_f2(self, nil), store))))
LEQ2(s1(n), s1(m)) -> LEQ2(n, m)
MAP_F2(pid, cons2(h, t)) -> MAP_F2(pid, t)
IF13(store, m, false) -> APP2(map_f2(self, nil), store)
The TRS R consists of the following rules:
fstsplit2(0, x) -> nil
fstsplit2(s1(n), nil) -> nil
fstsplit2(s1(n), cons2(h, t)) -> cons2(h, fstsplit2(n, t))
sndsplit2(0, x) -> x
sndsplit2(s1(n), nil) -> nil
sndsplit2(s1(n), cons2(h, t)) -> sndsplit2(n, t)
empty1(nil) -> true
empty1(cons2(h, t)) -> false
leq2(0, m) -> true
leq2(s1(n), 0) -> false
leq2(s1(n), s1(m)) -> leq2(n, m)
length1(nil) -> 0
length1(cons2(h, t)) -> s1(length1(t))
app2(nil, x) -> x
app2(cons2(h, t), x) -> cons2(h, app2(t, x))
map_f2(pid, nil) -> nil
map_f2(pid, cons2(h, t)) -> app2(f2(pid, h), map_f2(pid, t))
process2(store, m) -> if13(store, m, leq2(m, length1(store)))
if13(store, m, true) -> if23(store, m, empty1(fstsplit2(m, store)))
if13(store, m, false) -> if33(store, m, empty1(fstsplit2(m, app2(map_f2(self, nil), store))))
if23(store, m, false) -> process2(app2(map_f2(self, nil), sndsplit2(m, store)), m)
if33(store, m, false) -> process2(sndsplit2(m, app2(map_f2(self, nil), store)), m)
The set Q consists of the following terms:
fstsplit2(0, x0)
fstsplit2(s1(x0), nil)
fstsplit2(s1(x0), cons2(x1, x2))
sndsplit2(0, x0)
sndsplit2(s1(x0), nil)
sndsplit2(s1(x0), cons2(x1, x2))
empty1(nil)
empty1(cons2(x0, x1))
leq2(0, x0)
leq2(s1(x0), 0)
leq2(s1(x0), s1(x1))
length1(nil)
length1(cons2(x0, x1))
app2(nil, x0)
app2(cons2(x0, x1), x2)
map_f2(x0, nil)
map_f2(x0, cons2(x1, x2))
process2(x0, x1)
if13(x0, x1, true)
if13(x0, x1, false)
if23(x0, x1, false)
if33(x0, x1, false)
We have to consider all minimal (P,Q,R)-chains.
↳ QTRS
↳ Non-Overlap Check
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
Q DP problem:
The TRS P consists of the following rules:
IF33(store, m, false) -> SNDSPLIT2(m, app2(map_f2(self, nil), store))
PROCESS2(store, m) -> LENGTH1(store)
SNDSPLIT2(s1(n), cons2(h, t)) -> SNDSPLIT2(n, t)
IF23(store, m, false) -> PROCESS2(app2(map_f2(self, nil), sndsplit2(m, store)), m)
IF33(store, m, false) -> PROCESS2(sndsplit2(m, app2(map_f2(self, nil), store)), m)
IF23(store, m, false) -> APP2(map_f2(self, nil), sndsplit2(m, store))
IF13(store, m, true) -> FSTSPLIT2(m, store)
IF23(store, m, false) -> MAP_F2(self, nil)
MAP_F2(pid, cons2(h, t)) -> APP2(f2(pid, h), map_f2(pid, t))
IF13(store, m, true) -> EMPTY1(fstsplit2(m, store))
PROCESS2(store, m) -> IF13(store, m, leq2(m, length1(store)))
IF33(store, m, false) -> APP2(map_f2(self, nil), store)
FSTSPLIT2(s1(n), cons2(h, t)) -> FSTSPLIT2(n, t)
IF13(store, m, true) -> IF23(store, m, empty1(fstsplit2(m, store)))
IF13(store, m, false) -> MAP_F2(self, nil)
IF13(store, m, false) -> FSTSPLIT2(m, app2(map_f2(self, nil), store))
IF13(store, m, false) -> EMPTY1(fstsplit2(m, app2(map_f2(self, nil), store)))
APP2(cons2(h, t), x) -> APP2(t, x)
IF33(store, m, false) -> MAP_F2(self, nil)
LENGTH1(cons2(h, t)) -> LENGTH1(t)
IF23(store, m, false) -> SNDSPLIT2(m, store)
PROCESS2(store, m) -> LEQ2(m, length1(store))
IF13(store, m, false) -> IF33(store, m, empty1(fstsplit2(m, app2(map_f2(self, nil), store))))
LEQ2(s1(n), s1(m)) -> LEQ2(n, m)
MAP_F2(pid, cons2(h, t)) -> MAP_F2(pid, t)
IF13(store, m, false) -> APP2(map_f2(self, nil), store)
The TRS R consists of the following rules:
fstsplit2(0, x) -> nil
fstsplit2(s1(n), nil) -> nil
fstsplit2(s1(n), cons2(h, t)) -> cons2(h, fstsplit2(n, t))
sndsplit2(0, x) -> x
sndsplit2(s1(n), nil) -> nil
sndsplit2(s1(n), cons2(h, t)) -> sndsplit2(n, t)
empty1(nil) -> true
empty1(cons2(h, t)) -> false
leq2(0, m) -> true
leq2(s1(n), 0) -> false
leq2(s1(n), s1(m)) -> leq2(n, m)
length1(nil) -> 0
length1(cons2(h, t)) -> s1(length1(t))
app2(nil, x) -> x
app2(cons2(h, t), x) -> cons2(h, app2(t, x))
map_f2(pid, nil) -> nil
map_f2(pid, cons2(h, t)) -> app2(f2(pid, h), map_f2(pid, t))
process2(store, m) -> if13(store, m, leq2(m, length1(store)))
if13(store, m, true) -> if23(store, m, empty1(fstsplit2(m, store)))
if13(store, m, false) -> if33(store, m, empty1(fstsplit2(m, app2(map_f2(self, nil), store))))
if23(store, m, false) -> process2(app2(map_f2(self, nil), sndsplit2(m, store)), m)
if33(store, m, false) -> process2(sndsplit2(m, app2(map_f2(self, nil), store)), m)
The set Q consists of the following terms:
fstsplit2(0, x0)
fstsplit2(s1(x0), nil)
fstsplit2(s1(x0), cons2(x1, x2))
sndsplit2(0, x0)
sndsplit2(s1(x0), nil)
sndsplit2(s1(x0), cons2(x1, x2))
empty1(nil)
empty1(cons2(x0, x1))
leq2(0, x0)
leq2(s1(x0), 0)
leq2(s1(x0), s1(x1))
length1(nil)
length1(cons2(x0, x1))
app2(nil, x0)
app2(cons2(x0, x1), x2)
map_f2(x0, nil)
map_f2(x0, cons2(x1, x2))
process2(x0, x1)
if13(x0, x1, true)
if13(x0, x1, false)
if23(x0, x1, false)
if33(x0, x1, false)
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph contains 7 SCCs with 15 less nodes.
↳ QTRS
↳ Non-Overlap Check
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDPAfsSolverProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
APP2(cons2(h, t), x) -> APP2(t, x)
The TRS R consists of the following rules:
fstsplit2(0, x) -> nil
fstsplit2(s1(n), nil) -> nil
fstsplit2(s1(n), cons2(h, t)) -> cons2(h, fstsplit2(n, t))
sndsplit2(0, x) -> x
sndsplit2(s1(n), nil) -> nil
sndsplit2(s1(n), cons2(h, t)) -> sndsplit2(n, t)
empty1(nil) -> true
empty1(cons2(h, t)) -> false
leq2(0, m) -> true
leq2(s1(n), 0) -> false
leq2(s1(n), s1(m)) -> leq2(n, m)
length1(nil) -> 0
length1(cons2(h, t)) -> s1(length1(t))
app2(nil, x) -> x
app2(cons2(h, t), x) -> cons2(h, app2(t, x))
map_f2(pid, nil) -> nil
map_f2(pid, cons2(h, t)) -> app2(f2(pid, h), map_f2(pid, t))
process2(store, m) -> if13(store, m, leq2(m, length1(store)))
if13(store, m, true) -> if23(store, m, empty1(fstsplit2(m, store)))
if13(store, m, false) -> if33(store, m, empty1(fstsplit2(m, app2(map_f2(self, nil), store))))
if23(store, m, false) -> process2(app2(map_f2(self, nil), sndsplit2(m, store)), m)
if33(store, m, false) -> process2(sndsplit2(m, app2(map_f2(self, nil), store)), m)
The set Q consists of the following terms:
fstsplit2(0, x0)
fstsplit2(s1(x0), nil)
fstsplit2(s1(x0), cons2(x1, x2))
sndsplit2(0, x0)
sndsplit2(s1(x0), nil)
sndsplit2(s1(x0), cons2(x1, x2))
empty1(nil)
empty1(cons2(x0, x1))
leq2(0, x0)
leq2(s1(x0), 0)
leq2(s1(x0), s1(x1))
length1(nil)
length1(cons2(x0, x1))
app2(nil, x0)
app2(cons2(x0, x1), x2)
map_f2(x0, nil)
map_f2(x0, cons2(x1, x2))
process2(x0, x1)
if13(x0, x1, true)
if13(x0, x1, false)
if23(x0, x1, false)
if33(x0, x1, false)
We have to consider all minimal (P,Q,R)-chains.
By using an argument filtering and a montonic ordering, at least one Dependency Pair of this SCC can be strictly oriented.
APP2(cons2(h, t), x) -> APP2(t, x)
Used argument filtering: APP2(x1, x2) = x1
cons2(x1, x2) = cons1(x2)
Used ordering: Quasi Precedence:
trivial
↳ QTRS
↳ Non-Overlap Check
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDPAfsSolverProof
↳ QDP
↳ PisEmptyProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
Q DP problem:
P is empty.
The TRS R consists of the following rules:
fstsplit2(0, x) -> nil
fstsplit2(s1(n), nil) -> nil
fstsplit2(s1(n), cons2(h, t)) -> cons2(h, fstsplit2(n, t))
sndsplit2(0, x) -> x
sndsplit2(s1(n), nil) -> nil
sndsplit2(s1(n), cons2(h, t)) -> sndsplit2(n, t)
empty1(nil) -> true
empty1(cons2(h, t)) -> false
leq2(0, m) -> true
leq2(s1(n), 0) -> false
leq2(s1(n), s1(m)) -> leq2(n, m)
length1(nil) -> 0
length1(cons2(h, t)) -> s1(length1(t))
app2(nil, x) -> x
app2(cons2(h, t), x) -> cons2(h, app2(t, x))
map_f2(pid, nil) -> nil
map_f2(pid, cons2(h, t)) -> app2(f2(pid, h), map_f2(pid, t))
process2(store, m) -> if13(store, m, leq2(m, length1(store)))
if13(store, m, true) -> if23(store, m, empty1(fstsplit2(m, store)))
if13(store, m, false) -> if33(store, m, empty1(fstsplit2(m, app2(map_f2(self, nil), store))))
if23(store, m, false) -> process2(app2(map_f2(self, nil), sndsplit2(m, store)), m)
if33(store, m, false) -> process2(sndsplit2(m, app2(map_f2(self, nil), store)), m)
The set Q consists of the following terms:
fstsplit2(0, x0)
fstsplit2(s1(x0), nil)
fstsplit2(s1(x0), cons2(x1, x2))
sndsplit2(0, x0)
sndsplit2(s1(x0), nil)
sndsplit2(s1(x0), cons2(x1, x2))
empty1(nil)
empty1(cons2(x0, x1))
leq2(0, x0)
leq2(s1(x0), 0)
leq2(s1(x0), s1(x1))
length1(nil)
length1(cons2(x0, x1))
app2(nil, x0)
app2(cons2(x0, x1), x2)
map_f2(x0, nil)
map_f2(x0, cons2(x1, x2))
process2(x0, x1)
if13(x0, x1, true)
if13(x0, x1, false)
if23(x0, x1, false)
if33(x0, x1, false)
We have to consider all minimal (P,Q,R)-chains.
The TRS P is empty. Hence, there is no (P,Q,R) chain.
↳ QTRS
↳ Non-Overlap Check
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDPAfsSolverProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
MAP_F2(pid, cons2(h, t)) -> MAP_F2(pid, t)
The TRS R consists of the following rules:
fstsplit2(0, x) -> nil
fstsplit2(s1(n), nil) -> nil
fstsplit2(s1(n), cons2(h, t)) -> cons2(h, fstsplit2(n, t))
sndsplit2(0, x) -> x
sndsplit2(s1(n), nil) -> nil
sndsplit2(s1(n), cons2(h, t)) -> sndsplit2(n, t)
empty1(nil) -> true
empty1(cons2(h, t)) -> false
leq2(0, m) -> true
leq2(s1(n), 0) -> false
leq2(s1(n), s1(m)) -> leq2(n, m)
length1(nil) -> 0
length1(cons2(h, t)) -> s1(length1(t))
app2(nil, x) -> x
app2(cons2(h, t), x) -> cons2(h, app2(t, x))
map_f2(pid, nil) -> nil
map_f2(pid, cons2(h, t)) -> app2(f2(pid, h), map_f2(pid, t))
process2(store, m) -> if13(store, m, leq2(m, length1(store)))
if13(store, m, true) -> if23(store, m, empty1(fstsplit2(m, store)))
if13(store, m, false) -> if33(store, m, empty1(fstsplit2(m, app2(map_f2(self, nil), store))))
if23(store, m, false) -> process2(app2(map_f2(self, nil), sndsplit2(m, store)), m)
if33(store, m, false) -> process2(sndsplit2(m, app2(map_f2(self, nil), store)), m)
The set Q consists of the following terms:
fstsplit2(0, x0)
fstsplit2(s1(x0), nil)
fstsplit2(s1(x0), cons2(x1, x2))
sndsplit2(0, x0)
sndsplit2(s1(x0), nil)
sndsplit2(s1(x0), cons2(x1, x2))
empty1(nil)
empty1(cons2(x0, x1))
leq2(0, x0)
leq2(s1(x0), 0)
leq2(s1(x0), s1(x1))
length1(nil)
length1(cons2(x0, x1))
app2(nil, x0)
app2(cons2(x0, x1), x2)
map_f2(x0, nil)
map_f2(x0, cons2(x1, x2))
process2(x0, x1)
if13(x0, x1, true)
if13(x0, x1, false)
if23(x0, x1, false)
if33(x0, x1, false)
We have to consider all minimal (P,Q,R)-chains.
By using an argument filtering and a montonic ordering, at least one Dependency Pair of this SCC can be strictly oriented.
MAP_F2(pid, cons2(h, t)) -> MAP_F2(pid, t)
Used argument filtering: MAP_F2(x1, x2) = x2
cons2(x1, x2) = cons1(x2)
Used ordering: Quasi Precedence:
trivial
↳ QTRS
↳ Non-Overlap Check
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDPAfsSolverProof
↳ QDP
↳ PisEmptyProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
Q DP problem:
P is empty.
The TRS R consists of the following rules:
fstsplit2(0, x) -> nil
fstsplit2(s1(n), nil) -> nil
fstsplit2(s1(n), cons2(h, t)) -> cons2(h, fstsplit2(n, t))
sndsplit2(0, x) -> x
sndsplit2(s1(n), nil) -> nil
sndsplit2(s1(n), cons2(h, t)) -> sndsplit2(n, t)
empty1(nil) -> true
empty1(cons2(h, t)) -> false
leq2(0, m) -> true
leq2(s1(n), 0) -> false
leq2(s1(n), s1(m)) -> leq2(n, m)
length1(nil) -> 0
length1(cons2(h, t)) -> s1(length1(t))
app2(nil, x) -> x
app2(cons2(h, t), x) -> cons2(h, app2(t, x))
map_f2(pid, nil) -> nil
map_f2(pid, cons2(h, t)) -> app2(f2(pid, h), map_f2(pid, t))
process2(store, m) -> if13(store, m, leq2(m, length1(store)))
if13(store, m, true) -> if23(store, m, empty1(fstsplit2(m, store)))
if13(store, m, false) -> if33(store, m, empty1(fstsplit2(m, app2(map_f2(self, nil), store))))
if23(store, m, false) -> process2(app2(map_f2(self, nil), sndsplit2(m, store)), m)
if33(store, m, false) -> process2(sndsplit2(m, app2(map_f2(self, nil), store)), m)
The set Q consists of the following terms:
fstsplit2(0, x0)
fstsplit2(s1(x0), nil)
fstsplit2(s1(x0), cons2(x1, x2))
sndsplit2(0, x0)
sndsplit2(s1(x0), nil)
sndsplit2(s1(x0), cons2(x1, x2))
empty1(nil)
empty1(cons2(x0, x1))
leq2(0, x0)
leq2(s1(x0), 0)
leq2(s1(x0), s1(x1))
length1(nil)
length1(cons2(x0, x1))
app2(nil, x0)
app2(cons2(x0, x1), x2)
map_f2(x0, nil)
map_f2(x0, cons2(x1, x2))
process2(x0, x1)
if13(x0, x1, true)
if13(x0, x1, false)
if23(x0, x1, false)
if33(x0, x1, false)
We have to consider all minimal (P,Q,R)-chains.
The TRS P is empty. Hence, there is no (P,Q,R) chain.
↳ QTRS
↳ Non-Overlap Check
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDPAfsSolverProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
LENGTH1(cons2(h, t)) -> LENGTH1(t)
The TRS R consists of the following rules:
fstsplit2(0, x) -> nil
fstsplit2(s1(n), nil) -> nil
fstsplit2(s1(n), cons2(h, t)) -> cons2(h, fstsplit2(n, t))
sndsplit2(0, x) -> x
sndsplit2(s1(n), nil) -> nil
sndsplit2(s1(n), cons2(h, t)) -> sndsplit2(n, t)
empty1(nil) -> true
empty1(cons2(h, t)) -> false
leq2(0, m) -> true
leq2(s1(n), 0) -> false
leq2(s1(n), s1(m)) -> leq2(n, m)
length1(nil) -> 0
length1(cons2(h, t)) -> s1(length1(t))
app2(nil, x) -> x
app2(cons2(h, t), x) -> cons2(h, app2(t, x))
map_f2(pid, nil) -> nil
map_f2(pid, cons2(h, t)) -> app2(f2(pid, h), map_f2(pid, t))
process2(store, m) -> if13(store, m, leq2(m, length1(store)))
if13(store, m, true) -> if23(store, m, empty1(fstsplit2(m, store)))
if13(store, m, false) -> if33(store, m, empty1(fstsplit2(m, app2(map_f2(self, nil), store))))
if23(store, m, false) -> process2(app2(map_f2(self, nil), sndsplit2(m, store)), m)
if33(store, m, false) -> process2(sndsplit2(m, app2(map_f2(self, nil), store)), m)
The set Q consists of the following terms:
fstsplit2(0, x0)
fstsplit2(s1(x0), nil)
fstsplit2(s1(x0), cons2(x1, x2))
sndsplit2(0, x0)
sndsplit2(s1(x0), nil)
sndsplit2(s1(x0), cons2(x1, x2))
empty1(nil)
empty1(cons2(x0, x1))
leq2(0, x0)
leq2(s1(x0), 0)
leq2(s1(x0), s1(x1))
length1(nil)
length1(cons2(x0, x1))
app2(nil, x0)
app2(cons2(x0, x1), x2)
map_f2(x0, nil)
map_f2(x0, cons2(x1, x2))
process2(x0, x1)
if13(x0, x1, true)
if13(x0, x1, false)
if23(x0, x1, false)
if33(x0, x1, false)
We have to consider all minimal (P,Q,R)-chains.
By using an argument filtering and a montonic ordering, at least one Dependency Pair of this SCC can be strictly oriented.
LENGTH1(cons2(h, t)) -> LENGTH1(t)
Used argument filtering: LENGTH1(x1) = x1
cons2(x1, x2) = cons1(x2)
Used ordering: Quasi Precedence:
trivial
↳ QTRS
↳ Non-Overlap Check
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDPAfsSolverProof
↳ QDP
↳ PisEmptyProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
Q DP problem:
P is empty.
The TRS R consists of the following rules:
fstsplit2(0, x) -> nil
fstsplit2(s1(n), nil) -> nil
fstsplit2(s1(n), cons2(h, t)) -> cons2(h, fstsplit2(n, t))
sndsplit2(0, x) -> x
sndsplit2(s1(n), nil) -> nil
sndsplit2(s1(n), cons2(h, t)) -> sndsplit2(n, t)
empty1(nil) -> true
empty1(cons2(h, t)) -> false
leq2(0, m) -> true
leq2(s1(n), 0) -> false
leq2(s1(n), s1(m)) -> leq2(n, m)
length1(nil) -> 0
length1(cons2(h, t)) -> s1(length1(t))
app2(nil, x) -> x
app2(cons2(h, t), x) -> cons2(h, app2(t, x))
map_f2(pid, nil) -> nil
map_f2(pid, cons2(h, t)) -> app2(f2(pid, h), map_f2(pid, t))
process2(store, m) -> if13(store, m, leq2(m, length1(store)))
if13(store, m, true) -> if23(store, m, empty1(fstsplit2(m, store)))
if13(store, m, false) -> if33(store, m, empty1(fstsplit2(m, app2(map_f2(self, nil), store))))
if23(store, m, false) -> process2(app2(map_f2(self, nil), sndsplit2(m, store)), m)
if33(store, m, false) -> process2(sndsplit2(m, app2(map_f2(self, nil), store)), m)
The set Q consists of the following terms:
fstsplit2(0, x0)
fstsplit2(s1(x0), nil)
fstsplit2(s1(x0), cons2(x1, x2))
sndsplit2(0, x0)
sndsplit2(s1(x0), nil)
sndsplit2(s1(x0), cons2(x1, x2))
empty1(nil)
empty1(cons2(x0, x1))
leq2(0, x0)
leq2(s1(x0), 0)
leq2(s1(x0), s1(x1))
length1(nil)
length1(cons2(x0, x1))
app2(nil, x0)
app2(cons2(x0, x1), x2)
map_f2(x0, nil)
map_f2(x0, cons2(x1, x2))
process2(x0, x1)
if13(x0, x1, true)
if13(x0, x1, false)
if23(x0, x1, false)
if33(x0, x1, false)
We have to consider all minimal (P,Q,R)-chains.
The TRS P is empty. Hence, there is no (P,Q,R) chain.
↳ QTRS
↳ Non-Overlap Check
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDPAfsSolverProof
↳ QDP
↳ QDP
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
LEQ2(s1(n), s1(m)) -> LEQ2(n, m)
The TRS R consists of the following rules:
fstsplit2(0, x) -> nil
fstsplit2(s1(n), nil) -> nil
fstsplit2(s1(n), cons2(h, t)) -> cons2(h, fstsplit2(n, t))
sndsplit2(0, x) -> x
sndsplit2(s1(n), nil) -> nil
sndsplit2(s1(n), cons2(h, t)) -> sndsplit2(n, t)
empty1(nil) -> true
empty1(cons2(h, t)) -> false
leq2(0, m) -> true
leq2(s1(n), 0) -> false
leq2(s1(n), s1(m)) -> leq2(n, m)
length1(nil) -> 0
length1(cons2(h, t)) -> s1(length1(t))
app2(nil, x) -> x
app2(cons2(h, t), x) -> cons2(h, app2(t, x))
map_f2(pid, nil) -> nil
map_f2(pid, cons2(h, t)) -> app2(f2(pid, h), map_f2(pid, t))
process2(store, m) -> if13(store, m, leq2(m, length1(store)))
if13(store, m, true) -> if23(store, m, empty1(fstsplit2(m, store)))
if13(store, m, false) -> if33(store, m, empty1(fstsplit2(m, app2(map_f2(self, nil), store))))
if23(store, m, false) -> process2(app2(map_f2(self, nil), sndsplit2(m, store)), m)
if33(store, m, false) -> process2(sndsplit2(m, app2(map_f2(self, nil), store)), m)
The set Q consists of the following terms:
fstsplit2(0, x0)
fstsplit2(s1(x0), nil)
fstsplit2(s1(x0), cons2(x1, x2))
sndsplit2(0, x0)
sndsplit2(s1(x0), nil)
sndsplit2(s1(x0), cons2(x1, x2))
empty1(nil)
empty1(cons2(x0, x1))
leq2(0, x0)
leq2(s1(x0), 0)
leq2(s1(x0), s1(x1))
length1(nil)
length1(cons2(x0, x1))
app2(nil, x0)
app2(cons2(x0, x1), x2)
map_f2(x0, nil)
map_f2(x0, cons2(x1, x2))
process2(x0, x1)
if13(x0, x1, true)
if13(x0, x1, false)
if23(x0, x1, false)
if33(x0, x1, false)
We have to consider all minimal (P,Q,R)-chains.
By using an argument filtering and a montonic ordering, at least one Dependency Pair of this SCC can be strictly oriented.
LEQ2(s1(n), s1(m)) -> LEQ2(n, m)
Used argument filtering: LEQ2(x1, x2) = x2
s1(x1) = s1(x1)
Used ordering: Quasi Precedence:
trivial
↳ QTRS
↳ Non-Overlap Check
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDPAfsSolverProof
↳ QDP
↳ PisEmptyProof
↳ QDP
↳ QDP
↳ QDP
Q DP problem:
P is empty.
The TRS R consists of the following rules:
fstsplit2(0, x) -> nil
fstsplit2(s1(n), nil) -> nil
fstsplit2(s1(n), cons2(h, t)) -> cons2(h, fstsplit2(n, t))
sndsplit2(0, x) -> x
sndsplit2(s1(n), nil) -> nil
sndsplit2(s1(n), cons2(h, t)) -> sndsplit2(n, t)
empty1(nil) -> true
empty1(cons2(h, t)) -> false
leq2(0, m) -> true
leq2(s1(n), 0) -> false
leq2(s1(n), s1(m)) -> leq2(n, m)
length1(nil) -> 0
length1(cons2(h, t)) -> s1(length1(t))
app2(nil, x) -> x
app2(cons2(h, t), x) -> cons2(h, app2(t, x))
map_f2(pid, nil) -> nil
map_f2(pid, cons2(h, t)) -> app2(f2(pid, h), map_f2(pid, t))
process2(store, m) -> if13(store, m, leq2(m, length1(store)))
if13(store, m, true) -> if23(store, m, empty1(fstsplit2(m, store)))
if13(store, m, false) -> if33(store, m, empty1(fstsplit2(m, app2(map_f2(self, nil), store))))
if23(store, m, false) -> process2(app2(map_f2(self, nil), sndsplit2(m, store)), m)
if33(store, m, false) -> process2(sndsplit2(m, app2(map_f2(self, nil), store)), m)
The set Q consists of the following terms:
fstsplit2(0, x0)
fstsplit2(s1(x0), nil)
fstsplit2(s1(x0), cons2(x1, x2))
sndsplit2(0, x0)
sndsplit2(s1(x0), nil)
sndsplit2(s1(x0), cons2(x1, x2))
empty1(nil)
empty1(cons2(x0, x1))
leq2(0, x0)
leq2(s1(x0), 0)
leq2(s1(x0), s1(x1))
length1(nil)
length1(cons2(x0, x1))
app2(nil, x0)
app2(cons2(x0, x1), x2)
map_f2(x0, nil)
map_f2(x0, cons2(x1, x2))
process2(x0, x1)
if13(x0, x1, true)
if13(x0, x1, false)
if23(x0, x1, false)
if33(x0, x1, false)
We have to consider all minimal (P,Q,R)-chains.
The TRS P is empty. Hence, there is no (P,Q,R) chain.
↳ QTRS
↳ Non-Overlap Check
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDPAfsSolverProof
↳ QDP
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
SNDSPLIT2(s1(n), cons2(h, t)) -> SNDSPLIT2(n, t)
The TRS R consists of the following rules:
fstsplit2(0, x) -> nil
fstsplit2(s1(n), nil) -> nil
fstsplit2(s1(n), cons2(h, t)) -> cons2(h, fstsplit2(n, t))
sndsplit2(0, x) -> x
sndsplit2(s1(n), nil) -> nil
sndsplit2(s1(n), cons2(h, t)) -> sndsplit2(n, t)
empty1(nil) -> true
empty1(cons2(h, t)) -> false
leq2(0, m) -> true
leq2(s1(n), 0) -> false
leq2(s1(n), s1(m)) -> leq2(n, m)
length1(nil) -> 0
length1(cons2(h, t)) -> s1(length1(t))
app2(nil, x) -> x
app2(cons2(h, t), x) -> cons2(h, app2(t, x))
map_f2(pid, nil) -> nil
map_f2(pid, cons2(h, t)) -> app2(f2(pid, h), map_f2(pid, t))
process2(store, m) -> if13(store, m, leq2(m, length1(store)))
if13(store, m, true) -> if23(store, m, empty1(fstsplit2(m, store)))
if13(store, m, false) -> if33(store, m, empty1(fstsplit2(m, app2(map_f2(self, nil), store))))
if23(store, m, false) -> process2(app2(map_f2(self, nil), sndsplit2(m, store)), m)
if33(store, m, false) -> process2(sndsplit2(m, app2(map_f2(self, nil), store)), m)
The set Q consists of the following terms:
fstsplit2(0, x0)
fstsplit2(s1(x0), nil)
fstsplit2(s1(x0), cons2(x1, x2))
sndsplit2(0, x0)
sndsplit2(s1(x0), nil)
sndsplit2(s1(x0), cons2(x1, x2))
empty1(nil)
empty1(cons2(x0, x1))
leq2(0, x0)
leq2(s1(x0), 0)
leq2(s1(x0), s1(x1))
length1(nil)
length1(cons2(x0, x1))
app2(nil, x0)
app2(cons2(x0, x1), x2)
map_f2(x0, nil)
map_f2(x0, cons2(x1, x2))
process2(x0, x1)
if13(x0, x1, true)
if13(x0, x1, false)
if23(x0, x1, false)
if33(x0, x1, false)
We have to consider all minimal (P,Q,R)-chains.
By using an argument filtering and a montonic ordering, at least one Dependency Pair of this SCC can be strictly oriented.
SNDSPLIT2(s1(n), cons2(h, t)) -> SNDSPLIT2(n, t)
Used argument filtering: SNDSPLIT2(x1, x2) = x2
cons2(x1, x2) = cons1(x2)
Used ordering: Quasi Precedence:
trivial
↳ QTRS
↳ Non-Overlap Check
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDPAfsSolverProof
↳ QDP
↳ PisEmptyProof
↳ QDP
↳ QDP
Q DP problem:
P is empty.
The TRS R consists of the following rules:
fstsplit2(0, x) -> nil
fstsplit2(s1(n), nil) -> nil
fstsplit2(s1(n), cons2(h, t)) -> cons2(h, fstsplit2(n, t))
sndsplit2(0, x) -> x
sndsplit2(s1(n), nil) -> nil
sndsplit2(s1(n), cons2(h, t)) -> sndsplit2(n, t)
empty1(nil) -> true
empty1(cons2(h, t)) -> false
leq2(0, m) -> true
leq2(s1(n), 0) -> false
leq2(s1(n), s1(m)) -> leq2(n, m)
length1(nil) -> 0
length1(cons2(h, t)) -> s1(length1(t))
app2(nil, x) -> x
app2(cons2(h, t), x) -> cons2(h, app2(t, x))
map_f2(pid, nil) -> nil
map_f2(pid, cons2(h, t)) -> app2(f2(pid, h), map_f2(pid, t))
process2(store, m) -> if13(store, m, leq2(m, length1(store)))
if13(store, m, true) -> if23(store, m, empty1(fstsplit2(m, store)))
if13(store, m, false) -> if33(store, m, empty1(fstsplit2(m, app2(map_f2(self, nil), store))))
if23(store, m, false) -> process2(app2(map_f2(self, nil), sndsplit2(m, store)), m)
if33(store, m, false) -> process2(sndsplit2(m, app2(map_f2(self, nil), store)), m)
The set Q consists of the following terms:
fstsplit2(0, x0)
fstsplit2(s1(x0), nil)
fstsplit2(s1(x0), cons2(x1, x2))
sndsplit2(0, x0)
sndsplit2(s1(x0), nil)
sndsplit2(s1(x0), cons2(x1, x2))
empty1(nil)
empty1(cons2(x0, x1))
leq2(0, x0)
leq2(s1(x0), 0)
leq2(s1(x0), s1(x1))
length1(nil)
length1(cons2(x0, x1))
app2(nil, x0)
app2(cons2(x0, x1), x2)
map_f2(x0, nil)
map_f2(x0, cons2(x1, x2))
process2(x0, x1)
if13(x0, x1, true)
if13(x0, x1, false)
if23(x0, x1, false)
if33(x0, x1, false)
We have to consider all minimal (P,Q,R)-chains.
The TRS P is empty. Hence, there is no (P,Q,R) chain.
↳ QTRS
↳ Non-Overlap Check
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDPAfsSolverProof
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
FSTSPLIT2(s1(n), cons2(h, t)) -> FSTSPLIT2(n, t)
The TRS R consists of the following rules:
fstsplit2(0, x) -> nil
fstsplit2(s1(n), nil) -> nil
fstsplit2(s1(n), cons2(h, t)) -> cons2(h, fstsplit2(n, t))
sndsplit2(0, x) -> x
sndsplit2(s1(n), nil) -> nil
sndsplit2(s1(n), cons2(h, t)) -> sndsplit2(n, t)
empty1(nil) -> true
empty1(cons2(h, t)) -> false
leq2(0, m) -> true
leq2(s1(n), 0) -> false
leq2(s1(n), s1(m)) -> leq2(n, m)
length1(nil) -> 0
length1(cons2(h, t)) -> s1(length1(t))
app2(nil, x) -> x
app2(cons2(h, t), x) -> cons2(h, app2(t, x))
map_f2(pid, nil) -> nil
map_f2(pid, cons2(h, t)) -> app2(f2(pid, h), map_f2(pid, t))
process2(store, m) -> if13(store, m, leq2(m, length1(store)))
if13(store, m, true) -> if23(store, m, empty1(fstsplit2(m, store)))
if13(store, m, false) -> if33(store, m, empty1(fstsplit2(m, app2(map_f2(self, nil), store))))
if23(store, m, false) -> process2(app2(map_f2(self, nil), sndsplit2(m, store)), m)
if33(store, m, false) -> process2(sndsplit2(m, app2(map_f2(self, nil), store)), m)
The set Q consists of the following terms:
fstsplit2(0, x0)
fstsplit2(s1(x0), nil)
fstsplit2(s1(x0), cons2(x1, x2))
sndsplit2(0, x0)
sndsplit2(s1(x0), nil)
sndsplit2(s1(x0), cons2(x1, x2))
empty1(nil)
empty1(cons2(x0, x1))
leq2(0, x0)
leq2(s1(x0), 0)
leq2(s1(x0), s1(x1))
length1(nil)
length1(cons2(x0, x1))
app2(nil, x0)
app2(cons2(x0, x1), x2)
map_f2(x0, nil)
map_f2(x0, cons2(x1, x2))
process2(x0, x1)
if13(x0, x1, true)
if13(x0, x1, false)
if23(x0, x1, false)
if33(x0, x1, false)
We have to consider all minimal (P,Q,R)-chains.
By using an argument filtering and a montonic ordering, at least one Dependency Pair of this SCC can be strictly oriented.
FSTSPLIT2(s1(n), cons2(h, t)) -> FSTSPLIT2(n, t)
Used argument filtering: FSTSPLIT2(x1, x2) = x2
cons2(x1, x2) = cons1(x2)
Used ordering: Quasi Precedence:
trivial
↳ QTRS
↳ Non-Overlap Check
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDPAfsSolverProof
↳ QDP
↳ PisEmptyProof
↳ QDP
Q DP problem:
P is empty.
The TRS R consists of the following rules:
fstsplit2(0, x) -> nil
fstsplit2(s1(n), nil) -> nil
fstsplit2(s1(n), cons2(h, t)) -> cons2(h, fstsplit2(n, t))
sndsplit2(0, x) -> x
sndsplit2(s1(n), nil) -> nil
sndsplit2(s1(n), cons2(h, t)) -> sndsplit2(n, t)
empty1(nil) -> true
empty1(cons2(h, t)) -> false
leq2(0, m) -> true
leq2(s1(n), 0) -> false
leq2(s1(n), s1(m)) -> leq2(n, m)
length1(nil) -> 0
length1(cons2(h, t)) -> s1(length1(t))
app2(nil, x) -> x
app2(cons2(h, t), x) -> cons2(h, app2(t, x))
map_f2(pid, nil) -> nil
map_f2(pid, cons2(h, t)) -> app2(f2(pid, h), map_f2(pid, t))
process2(store, m) -> if13(store, m, leq2(m, length1(store)))
if13(store, m, true) -> if23(store, m, empty1(fstsplit2(m, store)))
if13(store, m, false) -> if33(store, m, empty1(fstsplit2(m, app2(map_f2(self, nil), store))))
if23(store, m, false) -> process2(app2(map_f2(self, nil), sndsplit2(m, store)), m)
if33(store, m, false) -> process2(sndsplit2(m, app2(map_f2(self, nil), store)), m)
The set Q consists of the following terms:
fstsplit2(0, x0)
fstsplit2(s1(x0), nil)
fstsplit2(s1(x0), cons2(x1, x2))
sndsplit2(0, x0)
sndsplit2(s1(x0), nil)
sndsplit2(s1(x0), cons2(x1, x2))
empty1(nil)
empty1(cons2(x0, x1))
leq2(0, x0)
leq2(s1(x0), 0)
leq2(s1(x0), s1(x1))
length1(nil)
length1(cons2(x0, x1))
app2(nil, x0)
app2(cons2(x0, x1), x2)
map_f2(x0, nil)
map_f2(x0, cons2(x1, x2))
process2(x0, x1)
if13(x0, x1, true)
if13(x0, x1, false)
if23(x0, x1, false)
if33(x0, x1, false)
We have to consider all minimal (P,Q,R)-chains.
The TRS P is empty. Hence, there is no (P,Q,R) chain.
↳ QTRS
↳ Non-Overlap Check
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
PROCESS2(store, m) -> IF13(store, m, leq2(m, length1(store)))
IF13(store, m, false) -> IF33(store, m, empty1(fstsplit2(m, app2(map_f2(self, nil), store))))
IF33(store, m, false) -> PROCESS2(sndsplit2(m, app2(map_f2(self, nil), store)), m)
IF23(store, m, false) -> PROCESS2(app2(map_f2(self, nil), sndsplit2(m, store)), m)
IF13(store, m, true) -> IF23(store, m, empty1(fstsplit2(m, store)))
The TRS R consists of the following rules:
fstsplit2(0, x) -> nil
fstsplit2(s1(n), nil) -> nil
fstsplit2(s1(n), cons2(h, t)) -> cons2(h, fstsplit2(n, t))
sndsplit2(0, x) -> x
sndsplit2(s1(n), nil) -> nil
sndsplit2(s1(n), cons2(h, t)) -> sndsplit2(n, t)
empty1(nil) -> true
empty1(cons2(h, t)) -> false
leq2(0, m) -> true
leq2(s1(n), 0) -> false
leq2(s1(n), s1(m)) -> leq2(n, m)
length1(nil) -> 0
length1(cons2(h, t)) -> s1(length1(t))
app2(nil, x) -> x
app2(cons2(h, t), x) -> cons2(h, app2(t, x))
map_f2(pid, nil) -> nil
map_f2(pid, cons2(h, t)) -> app2(f2(pid, h), map_f2(pid, t))
process2(store, m) -> if13(store, m, leq2(m, length1(store)))
if13(store, m, true) -> if23(store, m, empty1(fstsplit2(m, store)))
if13(store, m, false) -> if33(store, m, empty1(fstsplit2(m, app2(map_f2(self, nil), store))))
if23(store, m, false) -> process2(app2(map_f2(self, nil), sndsplit2(m, store)), m)
if33(store, m, false) -> process2(sndsplit2(m, app2(map_f2(self, nil), store)), m)
The set Q consists of the following terms:
fstsplit2(0, x0)
fstsplit2(s1(x0), nil)
fstsplit2(s1(x0), cons2(x1, x2))
sndsplit2(0, x0)
sndsplit2(s1(x0), nil)
sndsplit2(s1(x0), cons2(x1, x2))
empty1(nil)
empty1(cons2(x0, x1))
leq2(0, x0)
leq2(s1(x0), 0)
leq2(s1(x0), s1(x1))
length1(nil)
length1(cons2(x0, x1))
app2(nil, x0)
app2(cons2(x0, x1), x2)
map_f2(x0, nil)
map_f2(x0, cons2(x1, x2))
process2(x0, x1)
if13(x0, x1, true)
if13(x0, x1, false)
if23(x0, x1, false)
if33(x0, x1, false)
We have to consider all minimal (P,Q,R)-chains.